Remove _PREDICATE sort #2719

ttuegel · 2021-06-30T02:22:55Z

Opening a new pull request to avoid spamming the original author with notifications.

Review checklist

The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.

Summary. Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history.
Documentation. Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing.
Tests. Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests.
Clean up. The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes!

Remove the predicate sort in favour of using known sorts at all call sites. This mostly adds sort arguments to various functions that previously implicitly used _PREDICATE sort. In turn this means removing the various underbar methods previously in `Kore.Internal.TermLike`.

github-actions · 2021-08-11T12:30:50Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-pop1.sh	-0.003847	-0.004854
test/regression-evm/test-straight-line.sh	-0.003739	-0.005195
test/regression-evm/test-straight-line-no-invalid.sh	-0.003680	-0.004910
test/regression-evm/test-branching-invalid.sh	-0.004121	-0.005313
test/regression-evm/test-sum-to-n.sh	-0.016360	0.110953
test/regression-evm/test-branching-no-invalid.sh	-0.004071	0.019726
test/regression-evm/test-add0.sh	-0.004196	-0.016149
test/regression-evm/test-sumTo10.sh	-0.007471	0.004080
test/regression-wasm/test-memory.sh	-0.007040	-0.021684
test/regression-wasm/test-locals.sh	-0.004711	-0.021793
test/regression-wasm/test-wrc20.sh	-0.007667	0.020088
test/regression-wasm/test-loops.sh	-0.009567	-0.021429
test/regression-wasm/test-simple-arithmetic.sh	-0.005581	-0.021560

github-actions · 2021-08-12T09:12:45Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-pop1.sh	-0.003847	-0.000758
test/regression-evm/test-straight-line.sh	-0.003739	0.005956
test/regression-evm/test-straight-line-no-invalid.sh	-0.003680	0.008287
test/regression-evm/test-branching-invalid.sh	-0.004121	-0.000425
test/regression-evm/test-sum-to-n.sh	-0.016353	0.008670
test/regression-evm/test-branching-no-invalid.sh	-0.004071	0.019724
test/regression-evm/test-add0.sh	-0.004196	-0.000615
test/regression-evm/test-sumTo10.sh	-0.007471	0.003459
test/regression-wasm/test-memory.sh	-0.007042	-0.021684
test/regression-wasm/test-locals.sh	-0.004711	-0.021792
test/regression-wasm/test-wrc20.sh	-0.007698	0.005233
test/regression-wasm/test-loops.sh	-0.009587	-0.021428
test/regression-wasm/test-simple-arithmetic.sh	-0.005506	-0.021340

ana-pantilie · 2021-08-13T09:48:08Z

kore/src/Kore/Internal/Predicate.hs

-            , Pretty.indent 4 (unparse $ fromPredicate_ <$> termLikeF)
+            , Pretty.indent
+                4
+                (unparse $ fromPredicate (mkSortVariable "_") <$> termLikeF)


Why not call pretty directly instead of fromPredicate and unparse?

termLikeF is a TermLikeF variable (Predicate variable). TermLikeF doesn't have a Pretty instance, and the use of its Unparse instance would require Predicate to have an Unparse instance as well.

Ah, I see. Thanks for explaning!

ana-pantilie · 2021-08-13T09:48:48Z

kore/src/Kore/Internal/Predicate.hs

        )
  where
-    term = fromPredicate_ (synthesize predF)
+    term = fromPredicate (mkSortVariable "_") (synthesize predF)


Same as above.

ana-pantilie · 2021-08-13T09:52:00Z

kore/src/Kore/Internal/SideCondition.hs

            case predicate of
                PredicateEquals t1 t2 ->
-                    case retractLocalFunction (TermLike.mkEquals_ t1 t2) of
+                    case retractLocalFunction (TermLike.mkEquals (TermLike.termLikeSort t1) t1 t2) of


I think retractLocalFunction should take a Predicate instead of a TermLike, so we should construct a Predicate \\equals here between the two terms, and send it to retractLocalFunction.

ana-pantilie · 2021-08-13T09:55:40Z

kore/src/Kore/Repl/Interpreter.hs

            , provenValue = makeAuxReplOutput "Proven."
            }
  where
+    -- Dummy sort used to unparse configurations.


I wouldn't call this a "dummy sort", it's just a variable.

Suggested change

-- Dummy sort used to unparse configurations.

-- Sort variable used to unparse configurations.

ana-pantilie · 2021-08-13T09:57:34Z

kore/src/Kore/Rewrite/Implication.hs

            } = implication'
+        rightTerm =
+            case OrPattern.tryGetSort right of
+                Nothing -> error "to do"


This shouldn't be an error, right?

ana-pantilie · 2021-08-13T10:16:04Z

kore/src/Kore/Simplify/AndTerms.hs

            lift $ Builtin.Map.unifyEquals childTransformers tools unifyData
        | Just unifyData <- Builtin.Map.matchUnifyNotInKeys first second =
-            lift $ Builtin.Map.unifyNotInKeys childTransformers notSimplifier unifyData
+            lift $ Builtin.Map.unifyNotInKeys (termLikeSort first) childTransformers notSimplifier unifyData


Same question as above.

ana-pantilie · 2021-08-13T10:28:50Z

kore/src/Kore/Simplify/TermLike.hs

                AndF andF -> do
                    let conjuncts = foldMap MultiAnd.fromTermLike andF
-                    And.simplify Not.notSimplifier sideCondition
+                    And.simplify sort Not.notSimplifier sideCondition


I think it's a little weird and inconsistent that some of the simplifiers take that sort argument while others don't. Is there any reason for this?

And.makeEvaluate might receive an empty MultiAnd, so this pr gave it a Sort parameter in order to be able to return a \top. And.simplify calls And.makeEvaluate, but its MultiAnd (OrPattern RewritingVariableName) might not contain any Pattern either. That's why now it has a Sort parameter.

I understand. Could you add a small comment in each place where the sort argument is needed? For example, here we can say "MultiAnd doesn't preserve the sort so we need to send it as an external argument".

Could you add ^?

Edit: sorry, the comment isn't visible in the review. Please take a look at my responses to our discussions above.

ana-pantilie · 2021-08-13T10:29:21Z

kore/src/Kore/Simplify/Top.hs

    Top Sort child ->
    OrPattern RewritingVariableName
-simplify _ = OrPattern.top
+simplify sort _ = OrPattern.topOf sort


Why not just get the sort from the Top Sort child type?

ana-pantilie · 2021-08-13T12:11:47Z

kore/test/Test/Kore/Builtin/KEqual.hs

+                mkEquals
+                    kSort


I was thinking about this, and I want to be 100% sure I understand this. I'd expect the ==_ (where _ is K, Int etc.) to return a Bool. The reason this doesn't return Bool here but kSort is because \\equals is a predicate and we can give it any result sort. If we did \\and unification instead, the resulting sort would be Bool, right?

Yes, if I replace mkEquals with mkAnd, the result sort is Bool

Cool. Could you add some similar tests with mkAnd as well?

ana-pantilie · 2021-08-13T12:23:28Z

kore/test/Test/Kore/Simplify/Or.hs

                [ prettyOr or1 or2
                , "to become:"
-                , Unparser.unparse $ OrPattern.toTermLike expected
+                , Unparser.unparse $ OrPattern.toTermLike (mkSortVariable "_") expected


If we have a sort here, we should use that. I guess we should use a sort variable only if the OrPattern is \\bottom.

RaoulSchaffranek · 2021-08-16T09:35:12Z

kore/test/Test/Kore/Builtin/Builtin.hs

+evaluateExpectTopK ::
+    (MonadSMT smt, MonadLog smt, MonadProf smt, MonadMask smt) =>
+    TermLike RewritingVariableName ->
+    Hedgehog.PropertyT smt ()
+evaluateExpectTopK termLike = do
+    actual <- evaluateT termLike
+    OrPattern.topOf kSort Hedgehog.=== actual
+


Let us give this function the HasCallStack constraint. This allows the test-suite to print more precise source locations of failed tests.

RaoulSchaffranek · 2021-08-16T10:09:50Z

kore/src/Kore/Simplify/Equals.hs

+        (first', second') =
+            minMaxBy (on compareForEquals (OrPattern.toTermLike sort)) first second

 {- TODO (virgil): Preserve pattern sorts under simplification.


I think this change resolves the TODO from the comment, so we should remove it.

RaoulSchaffranek · 2021-08-16T10:17:59Z

kore/src/Kore/Simplify/Equals.hs

-            secondCeil <- makeEvaluateCeil sideCondition second'
-            firstCeilNegation <- Not.simplifyEvaluated sideCondition firstCeil
-            secondCeilNegation <- Not.simplifyEvaluated sideCondition secondCeil
+            let termSort = termLikeSort firstTerm


Is there a difference between termSort and sort from the where-clause? Otherwise, I'd suggest keeping only one definition.

github-actions · 2021-08-16T12:47:08Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-pop1.sh	-0.004091	0.003787
test/regression-evm/test-straight-line.sh	-0.003940	0.000310
test/regression-evm/test-straight-line-no-invalid.sh	-0.003881	0.024561
test/regression-evm/test-branching-invalid.sh	-0.004353	0.018583
test/regression-evm/test-sum-to-n.sh	-0.024183	0.004238
test/regression-evm/test-branching-no-invalid.sh	-0.004294	-0.011724
test/regression-evm/test-add0.sh	-0.004427	-0.000801
test/regression-evm/test-sumTo10.sh	-0.007893	-0.003546
test/regression-wasm/test-memory.sh	-0.008694	-0.021852
test/regression-wasm/test-locals.sh	-0.005145	-0.021150
test/regression-wasm/test-wrc20.sh	-0.009926	0.003112
test/regression-wasm/test-loops.sh	-0.012111	-0.021469
test/regression-wasm/test-simple-arithmetic.sh	-0.006361	-0.021202

github-actions · 2021-08-16T12:55:22Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-pop1.sh	-0.004071	0.014048
test/regression-evm/test-straight-line.sh	-0.003940	0.000310
test/regression-evm/test-straight-line-no-invalid.sh	-0.003882	0.013606
test/regression-evm/test-branching-invalid.sh	-0.004353	0.012607
test/regression-evm/test-sum-to-n.sh	-0.024169	-0.006507
test/regression-evm/test-branching-no-invalid.sh	-0.004294	-0.011726
test/regression-evm/test-add0.sh	-0.004427	-0.000801
test/regression-evm/test-sumTo10.sh	-0.007894	-0.005123
test/regression-wasm/test-memory.sh	-0.008654	-0.021853
test/regression-wasm/test-locals.sh	-0.005144	-0.021149
test/regression-wasm/test-wrc20.sh	-0.009810	0.021128
test/regression-wasm/test-loops.sh	-0.012033	-0.021469
test/regression-wasm/test-simple-arithmetic.sh	-0.006358	-0.021256

ana-pantilie · 2021-08-16T14:18:03Z

kore/src/Kore/Builtin/AssociativeCommutative.hs

-            case elementListAsInternal tools (termLikeSort first) remainder2Terms of
+            case elementListAsInternal
+                tools
+                (sameSort (termLikeSort first) (termLikeSort first))


Did you mean

Suggested change

(sameSort (termLikeSort first) (termLikeSort first))

(sameSort (termLikeSort first) (termLikeSort second))

ana-pantilie · 2021-08-16T14:18:36Z

kore/src/Kore/Builtin/EqTerm.hs

-
-This function is suitable only for equality simplification.
-}
-unifyEqTerm ::


Where did this go?

ana-pantilie · 2021-08-16T14:22:55Z

kore/src/Kore/Simplify/AndTerms.hs

-            lift $ bottomTermEquals SideCondition.topTODO unifyData
+            lift $
+                bottomTermEquals
+                    (sameSort (termLikeSort first) (termLikeSort first))


This is checking first and first again.

ana-pantilie · 2021-08-16T14:23:01Z

kore/src/Kore/Simplify/AndTerms.hs

-            lift $ Builtin.Map.unifyNotInKeys childTransformers notSimplifier unifyData
+            lift $
+                Builtin.Map.unifyNotInKeys
+                    (sameSort (termLikeSort first) (termLikeSort first))


This is checking first and first again.

ana-pantilie · 2021-08-16T14:26:10Z

kore/src/Kore/Simplify/TermLike.hs

                AndF andF -> do
                    let conjuncts = foldMap MultiAnd.fromTermLike andF
-                    And.simplify Not.notSimplifier sideCondition
+                    And.simplify sort Not.notSimplifier sideCondition


Could you add ^?

Edit: sorry, the comment isn't visible in the review. Please take a look at my responses to our discussions above.

github-actions · 2021-08-17T12:34:49Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-pop1.sh	-0.004066	0.008987
test/regression-evm/test-straight-line.sh	-0.003938	-0.004452
test/regression-evm/test-straight-line-no-invalid.sh	-0.003878	0.013606
test/regression-evm/test-branching-invalid.sh	-0.004350	0.003323
test/regression-evm/test-sum-to-n.sh	-0.024168	-0.001223
test/regression-evm/test-branching-no-invalid.sh	-0.004291	-0.011725
test/regression-evm/test-add0.sh	-0.004425	-0.000800
test/regression-evm/test-sumTo10.sh	-0.007889	-0.002923
test/regression-wasm/test-memory.sh	-0.008653	-0.021852
test/regression-wasm/test-locals.sh	-0.005139	-0.021150
test/regression-wasm/test-wrc20.sh	-0.009798	0.000215
test/regression-wasm/test-loops.sh	-0.012021	-0.021468
test/regression-wasm/test-simple-arithmetic.sh	-0.006323	-0.021202

github-actions · 2021-08-17T13:08:42Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-pop1.sh	-0.004066	-0.001280
test/regression-evm/test-straight-line.sh	-0.003938	-0.004452
test/regression-evm/test-straight-line-no-invalid.sh	-0.003878	0.013605
test/regression-evm/test-branching-invalid.sh	-0.004350	0.008598
test/regression-evm/test-sum-to-n.sh	-0.024174	-0.001223
test/regression-evm/test-branching-no-invalid.sh	-0.004292	-0.005860
test/regression-evm/test-add0.sh	-0.004425	-0.000802
test/regression-evm/test-sumTo10.sh	-0.007891	-0.002619
test/regression-wasm/test-memory.sh	-0.008650	-0.021854
test/regression-wasm/test-locals.sh	-0.005139	-0.021150
test/regression-wasm/test-wrc20.sh	-0.009809	-0.028056
test/regression-wasm/test-loops.sh	-0.011981	-0.021468
test/regression-wasm/test-simple-arithmetic.sh	-0.006273	-0.021202

github-actions · 2021-08-17T17:33:54Z

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-pop1.sh	-0.004066	0.018629
test/regression-evm/test-straight-line.sh	-0.003946	-0.000575
test/regression-evm/test-straight-line-no-invalid.sh	-0.003854	0.011004
test/regression-evm/test-branching-invalid.sh	-0.004349	0.019923
test/regression-evm/test-sum-to-n.sh	-0.024153	-0.006386
test/regression-evm/test-branching-no-invalid.sh	-0.004294	0.019886
test/regression-evm/test-add0.sh	-0.004425	0.006251
test/regression-evm/test-sumTo10.sh	-0.007885	-0.003810
test/regression-wasm/test-memory.sh	-0.008583	0.000238
test/regression-wasm/test-locals.sh	-0.005141	-0.000002
test/regression-wasm/test-wrc20.sh	-0.010605	-0.003598
test/regression-wasm/test-loops.sh	-0.012029	-0.080699
test/regression-wasm/test-simple-arithmetic.sh	-0.006295	-0.000102

Boarders and others added 30 commits June 26, 2021 13:45

Kore.Repl.Interpreter: Unparse \bottom with variable sort

27cca02

Kore.Exec: Unparse \bottom with variable sort

7668b69

Test.Kore.ASTVerifier.DefinitionVerifier.Imports: Use explicit sorts

bcab28c

Test.Kore.Step.Simplification.Forall: Use explicit sorts

25457c7

Test.Kore.Step.Simplification.InternalList: Use explicit sorts

20fb406

Test.Kore.Step.Simplification.InternalMap: Use explicit sorts

35ecdf0

Test.Kore.Step.Simplification.InternalSet: Use explicit sorts

8592b92

Test.Kore.Step.Simplification.Top: Use explicit sorts

86dcdb6

Test.Kore.Step.Simplification.Bottom: Use explicit sorts

c3881c3

NotSimplifier: Use Not.simplify

5c06061

Test.Kore.Step.Simplification: Use explicit sorts

2468aae

Test.Kore.Step.Simplification.Floor: Use explicit sorts

6232819

Test.Kore.Step.Simplification.Equals: Use explicit sorts

e49b86e

Add instance Pretty (Pattern _)

8bb8a19

Test.Kore.Step.Simplification.AndTerms: Use explicit sorts

b07a43b

Test.Kore.Builtin.Int: Use explicit sorts

96d2b4c

Test.Kore.Exec: Use explicit sorts

41ff9fa

Test.Kore.Internal.Pattern: Use explicit sorts

29e6322

Test.Kore.Equation.Application: Use explicit sorts

2427530

Test.Kore.Internal.OrPattern: Use explicit sorts

8ee4b65

Test.Kore.Builtin.KEqual: Use explicit sorts

0f29ed6

Test.Kore.Builtin.List: Use explicit sorts

35121a4

Test.Kore.Builtin.Map: Use explicit sorts

69cb850

Test.Kore.Builtin.Set: Use explicit sorts

fe6a55f

Test.Kore.Builtin.String: Use explicit sorts

ec6d1c6

Test.Kore.Internal.Predicate: Use explicit sorts

21b019e

Test.Kore.Internal.SideCondition: Use explicit sorts

bb25388

Test.Kore.Reachability.Claim: Use explicit sorts

16e5599

Test.Kore.Reachability.OnePathStrategy: Use explicit sorts

f6ee902

ana-pantilie requested review from RaoulSchaffranek and ana-pantilie August 11, 2021 14:11

ana-pantilie reviewed Aug 13, 2021

View reviewed changes

Address some comments

394831b

RaoulSchaffranek approved these changes Aug 16, 2021

View reviewed changes

andreiburdusa and others added 7 commits August 16, 2021 13:42

Remove Sort parameter from Top.simplify

6fb683a

Remove Sort parameter from InternalSet.simplify

a978cf8

Use pattern sort in Or.hs if available

26415a9

Address Raoul's comments

d422354

Merge remote-tracking branch 'origin/master' into remove-predicate-sort

281cdc8

Format with fourmolu

18b05e9

Rebuild

574844a

ana-pantilie suggested changes Aug 16, 2021

View reviewed changes

andreiburdusa and others added 4 commits August 16, 2021 18:20

Use sameSort with different sorts

5e0be13

Address comments

2262f72

Format with fourmolu

43766a9

Rebuild

aa25723

ana-pantilie self-requested a review August 17, 2021 14:19

ana-pantilie approved these changes Aug 17, 2021

View reviewed changes

ana-pantilie added the automerge label Aug 17, 2021

Merge branch 'master' into remove-predicate-sort

55ffe77

rv-jenkins merged commit 6394bf2 into master Aug 17, 2021

rv-jenkins deleted the remove-predicate-sort branch August 17, 2021 18:10

	-- Dummy sort used to unparse configurations.
	-- Sort variable used to unparse configurations.

	(sameSort (termLikeSort first) (termLikeSort first))
	(sameSort (termLikeSort first) (termLikeSort second))

Remove _PREDICATE sort #2719

Remove _PREDICATE sort #2719

Uh oh!

Conversation

ttuegel commented Jun 30, 2021

Review checklist

Uh oh!

github-actions bot commented Aug 11, 2021

Uh oh!

github-actions bot commented Aug 12, 2021

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ana-pantilie Aug 16, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ana-pantilie Aug 16, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Aug 16, 2021

Uh oh!

github-actions bot commented Aug 16, 2021

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ana-pantilie Aug 16, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Aug 17, 2021

Uh oh!

github-actions bot commented Aug 17, 2021

Uh oh!

github-actions bot commented Aug 17, 2021

Uh oh!

Reviewers

Assignees

Labels

ana-pantilie Aug 16, 2021 •

edited

Loading

ana-pantilie Aug 16, 2021 •

edited

Loading

ana-pantilie Aug 16, 2021 •

edited

Loading